/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking.transition;

import caetus.modelChecking.goal.ModelGoalMap;
import caetus.modelChecking.goal.ModelGoalSecret;
import caetus.modelChecking.variable.ModelBaseVariable;
import caetus.modelChecking.variable.ModelVariable;
import java.util.List;

/**
 * Serves to prepare transations with as little code as possible.
 *
 * @author Josef Hertl
 */
public enum TransitionActionEnum {

    CHANGE_STATE {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            return "State' := " + intArgument;
        }
    },
    /**
     * arg0 - the sent variable, bool - if the variable is primed.
     */
    SEND_PLAIN {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            String result = "SND(" + variableArguments[0].getVariableName();
            if (boolArgument) {
                result += "'";
            }
            result += ")";
            return result;
        }
    },
    /**
     * arg0 - the sent variable, arg1 - the encrypting variable, bool - if sent
     * variable is primed.
     */
    SEND_ENCRYPTED {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            String result = "SND({" + variableArguments[0].getVariableName();
            if (boolArgument) {
                result += "'";
            }
            result += "}_" + variableArguments[1].getVariableName() + ")";
            return result;
        }
    },
    /**
     * arg0 - the generated variable. Always primed.
     */
    GENERATE {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            return variableArguments[0].getVariableName() + "' := new()";
        }
    },
    /**
     * arg0 - the generated private key. Always primed. Automatically assumes
     * the name of the corresponding public key is LPuK and it is primed.
     */
    GENERATE_PRIVATE_KEY {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            return variableArguments[0].getVariableName() + "' := inv(LPuK')";
        }
    },
    /**
     * arg0 - the secret variable, bool - if the secret variable is primed.
     */
    SECRET {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            ModelGoalSecret secret = ModelGoalMap.findSecretOfVariable((ModelBaseVariable) variableArguments[0]);
            if (secret != null) { //this should never be null, since encrypting value means it should be kept secret
                return secret.makeSecretClause(boolArgument);
            } else {
                return null;
            }
        }
    },
    /**
     * Adds all possible secret requirements to the transition. None are primed.
     * arg0 - the variable that should be excluded.
     */
    ALL_SECRETS {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            String result = "";
            List<ModelVariable> secrets = ModelGoalMap.getAllSecretVariables();
            boolean first = true;
            for (ModelVariable modelVariable : secrets) {
                ModelGoalSecret secret = ModelGoalMap.findSecretOfVariable((ModelBaseVariable) modelVariable);
                if ((variableArguments.length == 0 || !modelVariable.equals(variableArguments[0]))) {
                    if (!first) {
                        result += " /\\ ";
                    } else {
                        first = false;
                    }
                    result += secret.makeSecretClause(false);
                }
            }
            return result;
        }
    },
    /**
     * arg0 - the comamnd constant. Never primed.
     */
    RECEIVE_COMMAND {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            return "RCV(" + variableArguments[0].getVariableName() + ")";
        }
    },
    /**
     * arg0 - the received variable, bool - if the variable is primed.
     */
    RECEIVE_VARIABLE {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            String result = "RCV(" + variableArguments[0].getVariableName();
            if (boolArgument) {
                result += "'";
            }
            result += ")";
            return result;
        }
    },
    /**
     * arg0 - the received variable, arg1 - the condition boolean, bool - if the
     * variable is primed.
     */
    RECEIVE_VARIABLE_WITH_CONDITION {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            String result = "RCV(" + variableArguments[0].getVariableName();
            if (boolArgument) {
                result += "'";
            }
            result += ") /\\ " + variableArguments[1].getVariableName() + " = true";
            return result;
        }
    },
    /**
     * arg0 - the received command, arg1 - the received variable, bool - if the
     * variable is primed.
     */
    RECEIVE_COMMAND_WITH_VARIABLE {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            String result = "RCV(" + variableArguments[0].getVariableName() + "." + variableArguments[1].getVariableName();
            if (boolArgument) {
                result += "'";
            }
            result += ")";
            return result;
        }
    },
    /**
     * arg0 - the received command, arg1 - the boolean variable storing the
     * condition.
     */
    RECEIVE_COMMAND_WITH_CONDITION {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            String result = "RCV(" + variableArguments[0].getVariableName() + ") /\\ " + variableArguments[1].getVariableName() + " = 1";
            return result;
        }
    },
    /**
     * arg0 - the set variable.
     */
    SET_VARIABLE_TO_TRUE {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            String result = variableArguments[0].getVariableName() + "' := 1";
            return result;
        }
    },
    /**
     * arg0 - the set variable.
     */
    SET_VARIABLE_TO_FALSE {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            String result = variableArguments[0].getVariableName() + "' := 0";
            return result;
        }
    },
    /**
     * int - the requested state number.
     */
    IS_IN_STATE {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            return "State = " + intArgument;
        }
    },
    START {
        @Override
        public String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument) {
            return "RCV(start)";
        }
    },;

    /**
     * Performs the transition based off the given arguments.
     *
     * @param variableArguments The passed variables.
     * @param intArgument The passed int. Mostly used with states.
     * @param boolArgument The passed bool. Mostly to signal priming.
     * @return
     */
    public abstract String makeTransitionAction(ModelVariable[] variableArguments, int intArgument, boolean boolArgument);
}
